Add Erdős Problem 1128 (Prikry-Mills counterexample for monochromatic countable boxes)#3782
Add Erdős Problem 1128 (Prikry-Mills counterexample for monochromatic countable boxes)#3782henrykmichalewski wants to merge 5 commits into
Conversation
Formalises Problem 1128 on monochromatic countable boxes in 2-colourings of ω × ω × ω₁. The main theorem answers False via the Prikry-Mills (1978) construction, recorded as the unpublished lemma prikryMills (with `sorry`). Includes variants.two_dimensional_false formally disproving the naturally-false two-dimensional variant via the ordering colouring, plus four proved helper lemmas establishing countability and boundedness properties of ω₁. Reference: https://www.erdosproblems.com/1128 Assisted by Claude (Anthropic).
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
Paul-Lez
added
the
awaiting-author
mo271
removed
the
awaiting-author
There was a problem hiding this comment.
Per repo conventions, it should appear once - ideally only in the erdos_1128 theorem docstring. The module docstring should be trimmed to title + reference link.
| /-! | ||
| # Erdős Problem 1128 | ||
|
|
||
| **Verbatim statement (Erdős #1128, status R):** | ||
| > Let $A,B,C$ be three sets of cardinality $\aleph_1$. Is it true that, in any $2$-colouring of $A\times B\times C$, there must exist $A_1\subset A$, $B_1\subset B$, $C_1\subset C$, all of cardinality $\aleph_0$, such that $A_1\times B_1\times C_1$ is monochromatic? | ||
|
|
||
| **Source:** https://www.erdosproblems.com/1128 | ||
|
|
||
| **Notes:** SOLVED - $50 | ||
|
|
||
|
|
||
| *Reference:* [erdosproblems.com/1128](https://www.erdosproblems.com/1128) | ||
|
|
||
| Erdős offered a \$50 prize for the resolution of this problem. It was disproved by | ||
| Prikry and Mills (1978, unpublished). | ||
|
|
||
| ## Problem statement | ||
|
|
||
| Let $A$, $B$, $C$ be three sets each of cardinality $\aleph_1$. Is it true that in | ||
| any 2-colouring of $A \times B \times C$, there must exist $A_1 \subseteq A$, | ||
| $B_1 \subseteq B$, $C_1 \subseteq C$, all of cardinality $\aleph_0$, such that | ||
| $A_1 \times B_1 \times C_1$ is monochromatic? | ||
|
|
||
| **Answer: NO.** Prikry and Mills (1978) constructed a 2-colouring of $\omega_1^3$ | ||
| with no monochromatic countable combinatorial box. | ||
|
|
||
| ## Prikry–Mills construction (sketch) | ||
|
|
||
| One fixes a well-ordering of $\omega_1$ and defines the colouring using the | ||
| ordinal arithmetic of the three coordinates. In ZFC, such a colouring can be | ||
| built by transfinite induction along $\omega_1$, ensuring at each stage that | ||
| every potential countable box $A_1 \times B_1 \times C_1$ is "killed" (receives | ||
| both colours). The key counting argument is that $\omega_1$ has uncountable | ||
| cofinality: at each stage of the induction only countably many boxes need to be | ||
| handled, and the construction can proceed without contradiction. | ||
|
|
||
| ## Note on the 2D analogue | ||
|
|
||
| The file also contains a variant `two_dimensional` which claims that in 2D, | ||
| any 2-colouring of $\omega_1 \times \omega_1$ has an uncountable monochromatic | ||
| rectangle $A_1 \times B_1$. This statement appears to be **false** in ZFC: | ||
| the ordering coloring $f(\alpha, \beta) = 0 \text{ iff } \alpha < \beta$ | ||
| provides a counterexample, since any uncountable subset of $\omega_1$ is cofinal | ||
| and hence cannot be bounded away from any other uncountable set. | ||
| -/ |
There was a problem hiding this comment.
| /-! | |
| # Erdős Problem 1128 | |
| **Verbatim statement (Erdős #1128, status R):** | |
| > Let $A,B,C$ be three sets of cardinality $\aleph_1$. Is it true that, in any $2$-colouring of $A\times B\times C$, there must exist $A_1\subset A$, $B_1\subset B$, $C_1\subset C$, all of cardinality $\aleph_0$, such that $A_1\times B_1\times C_1$ is monochromatic? | |
| **Source:** https://www.erdosproblems.com/1128 | |
| **Notes:** SOLVED - $50 | |
| *Reference:* [erdosproblems.com/1128](https://www.erdosproblems.com/1128) | |
| Erdős offered a \$50 prize for the resolution of this problem. It was disproved by | |
| Prikry and Mills (1978, unpublished). | |
| ## Problem statement | |
| Let $A$, $B$, $C$ be three sets each of cardinality $\aleph_1$. Is it true that in | |
| any 2-colouring of $A \times B \times C$, there must exist $A_1 \subseteq A$, | |
| $B_1 \subseteq B$, $C_1 \subseteq C$, all of cardinality $\aleph_0$, such that | |
| $A_1 \times B_1 \times C_1$ is monochromatic? | |
| **Answer: NO.** Prikry and Mills (1978) constructed a 2-colouring of $\omega_1^3$ | |
| with no monochromatic countable combinatorial box. | |
| ## Prikry–Mills construction (sketch) | |
| One fixes a well-ordering of $\omega_1$ and defines the colouring using the | |
| ordinal arithmetic of the three coordinates. In ZFC, such a colouring can be | |
| built by transfinite induction along $\omega_1$, ensuring at each stage that | |
| every potential countable box $A_1 \times B_1 \times C_1$ is "killed" (receives | |
| both colours). The key counting argument is that $\omega_1$ has uncountable | |
| cofinality: at each stage of the induction only countably many boxes need to be | |
| handled, and the construction can proceed without contradiction. | |
| ## Note on the 2D analogue | |
| The file also contains a variant `two_dimensional` which claims that in 2D, | |
| any 2-colouring of $\omega_1 \times \omega_1$ has an uncountable monochromatic | |
| rectangle $A_1 \times B_1$. This statement appears to be **false** in ZFC: | |
| the ordering coloring $f(\alpha, \beta) = 0 \text{ iff } \alpha < \beta$ | |
| provides a counterexample, since any uncountable subset of $\omega_1$ is cofinal | |
| and hence cannot be bounded away from any other uncountable set. | |
| -/ | |
| /-! | |
| # Erdős Problem 1128 | |
| *Reference:* [erdosproblems.com/1128](https://www.erdosproblems.com/1128) | |
| -/ |
| These establish key countability and boundedness properties of ω₁. | ||
| -/ | ||
|
|
||
| private abbrev Omega1 := {o : Ordinal.{0} // o < (aleph 1).ord} |
There was a problem hiding this comment.
Let's not redefne ω₁ with this dubious definition which perhaps give the wrong universe level. Mathib's already sits in Type 0 which is probably what Prikry-Mills needs here.
Also: this will probably alow us to elminate all the lemmas below: they are only thin wrappers around existing mathlib api already.
this would als perhaps allow us to eliminate the two versions of Prikry Mills:
Keep one and derive the other, or just keep one. Since the auxiliary lemmas are stated in terms of Omega1, the explicit version is more natural as the base case.
| Erdős–Rado theorem $\omega_1 \to (\omega_1)^2_2$, which concerns unordered pairs. | ||
| -/ | ||
| @[category research solved, AMS 3 5] | ||
| theorem erdos_1128.variants.two_dimensional_false : |
There was a problem hiding this comment.
two_dimensional_false seems not super closely related to 1128, but I guess we can keep it...
mo271
added
the
awaiting-author
- Trim the module docstring to title + reference link per mo271's
literal suggestion, dropping the duplicated verbatim statement, the
Prikry-Mills construction sketch, and the 2D-analogue note
(the latter content already lives in the
erdos_1128.variants.two_dimensional_false theorem docstring).
- Add a TODO acknowledging mo271's suggestion to remove the local
Omega1 abbreviation in favour of a direct use of Mathlib's ω₁.
Attempted the swap to {o : Ordinal // o < ω₁} but mixing ω₁ with
(ℵ_ 1).ord triggers definitional-equality issues across the wrapper
lemmas and the Prikry-Mills proof; left as a follow-up rather than
risk a sorry-explosion in this PR.
Per mo271 the two_dimensional_false variant stays ("I guess we can
keep it").
|
Applied mo271's docstring-convention review pass in
Line 81 follow-up (replace local Build: |
Let's rather do the full refactor now instead of introducing the alternative |
… (CI) Per upstream main (PR google-deepmind#3829, CategoryDocstringLinter enabled), all theorem and lemma declarations now require both @[category ...] and @[AMS ...] attributes - even private auxiliary lemmas. The previous docstring-cleanup commit (663bcd6) didn't add these to the 5 private lemmas around the local `Omega1` abbrev, which broke CI. Added @[category API, AMS 5] to all 5 affected lemmas: - card_le_aleph0_of_lt_omega1 - countable_toType_of_lt_omega1 - countable_Iio_of_lt_omega1 - countable_Iio_omega1 - countable_subset_bdd This commit also includes the merge of upstream/main needed to pick up the linter strictening.
3 participants
Formalises Erdős Problem 1128: whether every 2-colouring of$\omega \times \omega \times \omega_1$ admits a monochromatic product $A \times B \times C$ with $A, B, C$ countably infinite.
Contents
False): the problem is resolved negatively via the Prikry-Mills (1978, unpublished) construction.prikryMillslemma (sorry): records the unpublished 1978 Prikry-Mills counterexample colouring.variants.two_dimensional_false: a formal disproof of the naturally-false two-dimensional variant using the ordering colouring oncard_le_aleph0_of_lt_omega1,countable_toType_of_lt_omega1,countable_Iio_of_lt_omega1,countable_Iio_omega1,countable_subset_bdd) used for the supporting infrastructure.Assisted by Claude (Anthropic).